(set-option :model_validate true)
(set-option :model true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i5 Int)
(declare-const i7 Int)
(declare-const i8 Int)
(declare-const i10 Int)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const i11 Int)
(declare-const v10 Bool)
(declare-const i12 Int)
(declare-const v12 Bool)
(declare-const v14 Bool)
(assert (or (and (=> (> i1 48) (> i1 48)) v0 (< 12 545) (distinct (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (<= i8 554) (distinct i5 831) v12 v2 (not (not v1)) v0 (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (=> v7 (> i1 48)) v6 (<= 60 i7)) v10) (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (> 60 i7)))
(assert-soft (or v14 (<= i0 20) (=> v7 (> i1 48))))
(assert-soft (or (< 12 545) v10 (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5)))
(assert (or (<= 60 i7) (and (=> (> i1 48) (> i1 48)) v0 (< 12 545) (distinct (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (<= i8 554) (distinct i5 831) v12 v2 (not (not v1)) v0 (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (=> v7 (> i1 48)) v6 (<= 60 i7)) v10) (<= i0 20)))
(assert (or (=> v7 (> i1 48)) v9 (and (=> (> i1 48) (> i1 48)) v0 (< 12 545) (distinct (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (<= i8 554) (distinct i5 831) v12 v2 (not (not v1)) v0 (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (=> v7 (> i1 48)) v6 (<= 60 i7)) v10)))
(assert (or (> 60 i7) (<= 60 i7) (>= i0 48)))
(assert-soft (or (distinct i5 831) (<= 60 i7) (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5)))
(assert-soft (or v10 (<= i0 20) v9))
(assert (or v10 (<= 60 i7) v10))
(assert (or (< 12 545) (and (=> (> i1 48) (> i1 48)) v0 (< 12 545) (distinct (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (<= i8 554) (distinct i5 831) v12 v2 (not (not v1)) v0 (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (=> v7 (> i1 48)) v6 (<= 60 i7)) v10) (> 60 i7)))
(assert (or v9 v9 v9))
(assert (or (>= i0 48) (and (=> (> i1 48) (> i1 48)) v0 (< 12 545) (distinct (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (<= i8 554) (distinct i5 831) v12 v2 (not (not v1)) v0 (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (=> v7 (> i1 48)) v6 (<= 60 i7)) v10) (>= i0 48)))
(assert (or (=> v7 (> i1 48)) v9 v9))
(assert (or (<= 60 i7) (distinct i5 831) (<= i0 20)))
(assert-soft (or (<= 60 i7) v10 (and (=> (> i1 48) (> i1 48)) v0 (< 12 545) (distinct (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (<= i8 554) (distinct i5 831) v12 v2 (not (not v1)) v0 (distinct (> i0 649) v1 (not v1) v0 (not v1) (>= i0 48) (> i0 649) v5) (=> v7 (> i1 48)) v6 (<= 60 i7)) v10)))
(assert-soft (or (>= i0 48) (distinct i5 831) v14))
(check-sat)